KernelBridge.lean defines a local `Kernel.IndepFun.comp` lemma that
duplicates mathlib's `ProbabilityTheory.Kernel.IndepFun.comp` (specialized
to ℝ-valued composition targets). It has zero callers in the codebase:
the `_indep.comp` calls in `Probability/CondIndep/Indicator.lean` and
`Probability/CondIndep/Basic.lean` are on plain `IndepFun` (measure-based),
which resolves to mathlib's `ProbabilityTheory.IndepFun.comp` — a different
lemma in a different namespace.

This delete is stronger than PR #16's autoGolf suggestion (which kept the
lemma as a thin wrapper). Since there is nothing to wrap to, removing it
outright is cleaner.

- Exchangeability/DeFinetti/ViaKoopman/KernelBridge.lean:
  - delete the 30-line proof + 10-line docstring (lines 181-219)
  - update the module docstring "Main results" bullet list to match

)

Mines safe-subset replacements from the PR #16 autoGolf draft and applies
them to current main, skipping the suspicious subset (lia / bare
assumption / Real.ext_cauchy / grind only on non-arithmetic goals).

`fun_prop` adoptions (replace hand-built `Measurable.const_mul +
Finset.measurable_sum + .comp` chains):

- `DeFinetti/ViaKoopman/BlockAverage.lean`     (1 site)
- `DeFinetti/ViaL2/BlockAvgDef.lean`           (1 site)
- `DeFinetti/ViaL2/AlphaConvergence.lean`      (2 sites)
- `DeFinetti/ViaL2/CesaroConvergence.lean`     (3 sites)
- `DeFinetti/ViaL2/DirectingMeasureIntegral.lean` (4 sites, incl. one
  Integrable wrap via `fun_prop`)
- `DeFinetti/ViaL2/MainConvergence.lean`       (1 site)
- `DeFinetti/ViaMartingale/PairLawEquality.lean` (1 site,
  `measurable_consRV` → fun_prop)
- `Ergodic/ShiftInvariantRepresentatives.lean` (1 site,
  `measurable_coe_real_ereal.comp …` → fun_prop)
- `Core.lean:683` — collapse `simpa using (show … from by fun_prop)` to
  bare `fun_prop`.

Named-lemma replacements:

- `DeFinetti/ViaL2/DirectingMeasureIntegral.lean` 2× hand-built
  `IsPiSystem` proof for `Set.range Iic` → `isPiSystem_Iic`.
- `Contractability.lean:perm_range_eq` — 4-line `ext`+`use`+`simp` →
  `Finset.image_univ_equiv σ`.

Minor `by exact` removals in `BlockAvgDef.lean`.

Out of scope (per the audit, suspicious-category from #16):
- `BlockAverage.lean:82` `congr 1; ring` → `lia` swap (opaque substitution
  on non-arithmetic context).
- The proof-golfing-branch reversion of #18's
  `exists_perm_extending_strictMono` refactor.

Net -62 lines across 10 files. Build clean (3527 jobs), axioms standard,
0 sorries. No statement or signature changes.

…Info (#112)

Eight LSP-verified proof-body shrinks in the files that the bulk autoGolf
run in PR #16 never reached. Each site was probed individually rather
than via `exact?` (which timed out on these measure-heavy goals).

* `Crossings/Pathwise.lean:54` `up_neg_flip_eq_down`:
  body collapses to `rfl` — `downcrossingsBefore` is definitionally
  `upcrossingsBefore (-b) (-a) (negProcess X)`, so both sides of the
  lemma unfold to the same `⨆ N, ...` term.
* `Crossings/Pathwise.lean:123` `upcrossingsBefore_congr`:
  four lines (`simp only`/`congr`/`ext`/`rw`) collapse to
  `simp [upcrossingsBefore, upperCrossingTime_congr h]`.
* `Reverse.lean:80` `revCEFinite_martingale`:
  inline the local `have : 𝔽 (N-i) ≤ 𝔽 (N-j)` into the final
  `condExp_condExp_of_le` call.
* `Crossings/Bounds.lean:45` `hL1_bdd`:
  drop the `simp only [revCEFinite]`; `eLpNorm_one_condExp_le_eLpNorm`
  unifies definitionally.
* `Crossings/AntitoneLimit.lean:350` `h_tower`:
  rewrite as a term-mode `fun n => condExp_condExp_of_le (iInf_le 𝔽 n)
  (h_le n)`.
* `Crossings/AntitoneLimit.lean:368` `hL1_conv_Xn`:
  six-line `have`/`simp_rw`/`exact` collapses to a single
  `simpa [hXn_def, eLpNorm_sub_comm] using hL1_conv`.
* `TripleLawDropInfo/PairLawHelpers.lean:40` `marginal_law_eq_of_pair_law`:
  five lines (two `have`s + final `rw`) become a single
  `simpa [Measure.map_map …] using congrArg (Measure.map Prod.snd) h_law`.
* `TripleLawDropInfo/DropInfo.lean:211` final square-zero step:
  the trailing `have : ... = 0; linarith` two-liner collapses to a single
  `nlinarith [sq_nonneg (μ₂ ω - μ₁ ω)]`.

Net: 6 files, +11 / −30 (−19 lines).